(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/lists/list.ma".
include "basics/logic.ma".

inductive lit : Type[0] ≝
  int : bool → nat → lit. 
  
inductive operator : Type[0] ≝
  par : operator
| copar : operator
| seq : operator.  

inductive struct : Type[0] ≝
|  unit : struct
|  atom : lit → struct
|  lista : operator → list struct → struct.

notation "+x" with precedence 80 for @{int true $x}.
notation "-x" with precedence 80 for @{int false $x}.
notation "∘" with precedence 80 for @{(unit))}.

(*Qui sarebbe bello poter usare i caratteri*)
notation "x+" with precedence 100 for @{((atom +($x)))}.  
notation "x^" with precedence 100 for @{((atom -($x)))}.

notation "x ≡ y" with precedence 45
  for @{struct_eq $x $y}.

inductive struct_eq : struct→ struct → Prop ≝ 
 | eqRif : ∀S1 .                  S1 ≡ S1
 | eqAss : ∀L1,L2,L3.∀O.          lista O (L1@L2@L3) ≡ lista O (L1@((lista O L2)::L3))  
 | eqComm : ∀S1,S2 .              S2 ≡ S1 → S1≡ S2
 | eqTrans : ∀S1,S2,S3.          S1 ≡ S2 → S2 ≡ S3 → S1 ≡ S3 
 | eqUnitLeft : ∀O.∀L.              lista O L ≡ lista O (∘::L)
 | eqSingleton : ∀O.∀S.              lista O [S] ≡ S
 | eqContext : ∀H1,H2.∀L1,L2.∀O.   H1 ≡ H2 → lista O L1 ≡ lista O L2 → lista O (H1::L1) ≡ lista O (H2::L2).
 
 lemma prova : ∀n,m.∀S1,S2.  S1=n+ → S2=m+ →( S1≡S2 → S1=S2).